Automatic Verification of Parametric Specifications with Complex Topologies
Identifieur interne : 003114 ( Main/Exploration ); précédent : 003113; suivant : 003115Automatic Verification of Parametric Specifications with Complex Topologies
Auteurs : Johannes Faber [Allemagne] ; Carsten Ihlemann [Allemagne] ; Swen Jacobs [Suisse] ; Viorica Sofronie-Stokkermans [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
Url:
DOI: 10.1007/978-3-642-16265-7_12
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003457
- to stream Istex, to step Curation: 003415
- to stream Istex, to step Checkpoint: 000876
- to stream Main, to step Merge: 003171
- to stream Main, to step Curation: 003114
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automatic Verification of Parametric Specifications with Complex Topologies</title><author><name sortKey="Faber, Johannes" sort="Faber, Johannes" uniqKey="Faber J" first="Johannes" last="Faber">Johannes Faber</name></author><author><name sortKey="Ihlemann, Carsten" sort="Ihlemann, Carsten" uniqKey="Ihlemann C" first="Carsten" last="Ihlemann">Carsten Ihlemann</name></author><author><name sortKey="Jacobs, Swen" sort="Jacobs, Swen" uniqKey="Jacobs S" first="Swen" last="Jacobs">Swen Jacobs</name></author><author><name sortKey="Sofronie Stokkermans, Viorica" sort="Sofronie Stokkermans, Viorica" uniqKey="Sofronie Stokkermans V" first="Viorica" last="Sofronie-Stokkermans">Viorica Sofronie-Stokkermans</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:DC62A4D086EFE75EA9DECED5BF6C5221A7604DD7</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/978-3-642-16265-7_12</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-1X6W2M2K-D/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003457</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003457</idno><idno type="wicri:Area/Istex/Curation">003415</idno><idno type="wicri:Area/Istex/Checkpoint">000876</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000876</idno><idno type="wicri:doubleKey">0302-9743:2010:Faber J:automatic:verification:of</idno><idno type="wicri:Area/Main/Merge">003171</idno><idno type="wicri:Area/Main/Curation">003114</idno><idno type="wicri:Area/Main/Exploration">003114</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automatic Verification of Parametric Specifications with Complex Topologies</title><author><name sortKey="Faber, Johannes" sort="Faber, Johannes" uniqKey="Faber J" first="Johannes" last="Faber">Johannes Faber</name><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Department of Computing Science, University of Oldenburg</wicri:regionArea><wicri:noRegion>University of Oldenburg</wicri:noRegion><wicri:noRegion>University of Oldenburg</wicri:noRegion></affiliation></author><author><name sortKey="Ihlemann, Carsten" sort="Ihlemann, Carsten" uniqKey="Ihlemann C" first="Carsten" last="Ihlemann">Carsten Ihlemann</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max-Planck-Institut für Informatik, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author><author><name sortKey="Jacobs, Swen" sort="Jacobs, Swen" uniqKey="Jacobs S" first="Swen" last="Jacobs">Swen Jacobs</name><affiliation wicri:level="1"><country xml:lang="fr">Suisse</country><wicri:regionArea>École Polytechnique Fédérale de Lausanne</wicri:regionArea></affiliation></author><author><name sortKey="Sofronie Stokkermans, Viorica" sort="Sofronie Stokkermans, Viorica" uniqKey="Sofronie Stokkermans V" first="Viorica" last="Sofronie-Stokkermans">Viorica Sofronie-Stokkermans</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max-Planck-Institut für Informatik, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Suisse</li></country><region><li>Sarre (Land)</li></region><settlement><li>Sarrebruck</li></settlement></list><tree><country name="Allemagne"><noRegion><name sortKey="Faber, Johannes" sort="Faber, Johannes" uniqKey="Faber J" first="Johannes" last="Faber">Johannes Faber</name></noRegion><name sortKey="Ihlemann, Carsten" sort="Ihlemann, Carsten" uniqKey="Ihlemann C" first="Carsten" last="Ihlemann">Carsten Ihlemann</name><name sortKey="Sofronie Stokkermans, Viorica" sort="Sofronie Stokkermans, Viorica" uniqKey="Sofronie Stokkermans V" first="Viorica" last="Sofronie-Stokkermans">Viorica Sofronie-Stokkermans</name></country><country name="Suisse"><noRegion><name sortKey="Jacobs, Swen" sort="Jacobs, Swen" uniqKey="Jacobs S" first="Swen" last="Jacobs">Swen Jacobs</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003114 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003114 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:DC62A4D086EFE75EA9DECED5BF6C5221A7604DD7
|texte= Automatic Verification of Parametric Specifications with Complex Topologies
}}
| This area was generated with Dilib version V0.6.33. |  |